/*Model: bridge.1.*/

CONST

MAX_P : 4;

TYPE
  n_max_p : 0..(MAX_P - 1);
  signal : boolean;
  soldier_n : 0..3 ;
  t_time : 0..60;
  torch : 0..1;
  right_soldier : 0..4;
  chan_t : record id:soldier_n; minutes:t_time; action:signal; end;
  time : 0..25;
  soldier_state : enum { left , go_right , go_left , right } ;
  soldier_time : 5..25;
  soldier_t : record s_time:soldier_time ; s_state:soldier_state; end;
  torch_process : enum { free , one , two , going }; 

VAR
  total_time : t_time;
  w_is_torch : torch;
  on_right : right_soldier;
  time1 : time;
  time2 : time;

/*channels*/
  lets_go : chan_t;
  wanna_go : chan_t;

/*processes*/ 
  torch_t : torch_process;
  soldier : array [ soldier_n ] of soldier_t;  

/***REGOLE DI TRANSIZIONE***/
/*BEGIN Torch RULES */

rule "free to one"
   ( torch_t = free & wanna_go.action ) ==>
  BEGIN  
    wanna_go.action := false;
    wanna_go.minutes := time1;
    torch_t := one;
  END;

rule "one to two"
  ( torch_t = one & wanna_go.action ) ==>
  BEGIN
       wanna_go.action := false;
       wanna_go.minutes := time2;
       torch_t := two;
  END;

rule "one to going"
   ( torch_t = one & !wanna_go.action ) ==>
    BEGIN
       torch_t := going;
     END;

rule "two to going time1 >= time2"
  ( torch_t = two & time1 >= time2 ) ==>
  BEGIN
    lets_go.action := true;
    torch_t := going;
  END;
  
rule "two to going time1<time2"
   ( torch_t = two & time1 < time2 ) ==>
   BEGIN
    lets_go.action := true;
    time1 := time2;
    time2 := 0;  
    torch_t := going;
  END;

rule "going to free"
  ( torch_t = going & total_time + time1 <= 60 ) ==>     
  BEGIN
    lets_go.action := true;
    total_time := total_time + time1;
    time1 := 0;
    w_is_torch := 1 - w_is_torch;
    torch_t := free;
END;

/*END TORCH rules */ 
/***soldier rule***/

ruleset i:n_max_p do

/* from left soldier N goto state go_right */
  rule "left"
    ( soldier[i].s_state = left & w_is_torch = 0 ) ==>
    BEGIN
      wanna_go.action := true;
      wanna_go.id := i;
      wanna_go.minutes := soldier[i].s_time;
      soldier[i].s_state := go_right;
         /*atomic { where_is_torch==0;wanna_go!5; }  goto go_right; */
END;

/*from go_right soldier N goto state right */
rule "go_right"
  ( soldier[i].s_state = go_right & lets_go.action ) ==>
  BEGIN
    lets_go.action := false;
    on_right := on_right + 1 ;
    soldier[i].s_state := right;         
        /*atomic { lets_go?0;on_right = on_right+1; }  goto right;*/
END;

/*from right soldier N goto state go_left */
rule "right"
  ( soldier[i].s_state = go_left & w_is_torch = 1 ) ==>
  BEGIN
    wanna_go.id := i;
    wanna_go.minutes := soldier[i].s_time;
    wanna_go.action := true;
    on_right := on_right - 1;
    soldier[i].s_state := go_left;   /*atomic {where_is_torch==1;wanna_go!5;on_right = on_right-1;}  goto go_left;*/
END;

/*from go_left soldier N goto state left */
rule "go_left"
  ( soldier[i].s_state = left & lets_go.action ) ==>  
   BEGIN
    lets_go.action := false;
    soldier[i].s_state := left;
END;
END;
/* END Soldiers RULES */
	
STARTSTATE
  BEGIN
  w_is_torch := 0;
  soldier[0].s_state := left;
  soldier[1].s_state := left;
  soldier[2].s_state := left;
  soldier[3].s_state := left;
  soldier[0].s_time := 5; 
  soldier[1].s_time := 10;
  soldier[2].s_time := 20;
  soldier[3].s_time := 25;
  time1 := 0;
  time2 := 0;
  on_right := 0;
  total_time := 0;
  lets_go.action := false;
  torch_t := free ;
  wanna_go.action := false;
  /*lets_go.id := 0;*/
  /*lets_go.minutes := 0;*/
  /*wanna_go.id := 0;*/
  /*wanna_go.minutes := 0;*/
END;

  INVARIANT "All soldiers are on the other side"
  !exists i:n_max_p do 
  ( on_right != 4 & total_time > 60 )
END;
